MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) , matrixMult#1(nil(), @m2) -> nil() } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , +^#(@x, @y) -> c_2(#add^#(@x, @y)) , computeLine^#(@line, @m, @acc) -> c_3(computeLine#1^#(@line, @acc, @m)) , computeLine#1^#(::(@x, @xs), @acc, @m) -> c_4(computeLine#2^#(@m, @acc, @x, @xs)) , computeLine#1^#(nil(), @acc, @m) -> c_5() , computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_6(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , computeLine#2^#(nil(), @acc, @x, @xs) -> c_7() , lineMult^#(@n, @l1, @l2) -> c_8(lineMult#1^#(@l1, @l2, @n)) , lineMult#1^#(::(@x, @xs), @l2, @n) -> c_9(lineMult#2^#(@l2, @n, @x, @xs)) , lineMult#1^#(nil(), @l2, @n) -> c_10() , lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_11(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys)) , lineMult#2^#(nil(), @n, @x, @xs) -> c_12(*^#(@x, @n), lineMult^#(@n, @xs, nil())) , matrixMult^#(@m1, @m2) -> c_13(matrixMult#1^#(@m1, @m2)) , matrixMult#1^#(::(@l, @ls), @m2) -> c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) , matrixMult#1^#(nil(), @m2) -> c_15() } Weak DPs: { #mult^#(#0(), #0()) -> c_16() , #mult^#(#0(), #neg(@y)) -> c_17() , #mult^#(#0(), #pos(@y)) -> c_18() , #mult^#(#neg(@x), #0()) -> c_19() , #mult^#(#neg(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_21(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_22() , #mult^#(#pos(@x), #neg(@y)) -> c_23(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_25() , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_27(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_28(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_29(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #natmult^#(#0(), @y) -> c_38() , #natmult^#(#s(@x), @y) -> c_39(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #pred^#(#0()) -> c_30() , #pred^#(#neg(#s(@x))) -> c_31() , #pred^#(#pos(#s(#0()))) -> c_32() , #pred^#(#pos(#s(#s(@x)))) -> c_33() , #succ^#(#0()) -> c_34() , #succ^#(#neg(#s(#0()))) -> c_35() , #succ^#(#neg(#s(#s(@x)))) -> c_36() , #succ^#(#pos(#s(@x))) -> c_37() , #natadd^#(#0(), @y) -> c_40() , #natadd^#(#s(@x), @y) -> c_41(#natadd^#(@x, @y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , +^#(@x, @y) -> c_2(#add^#(@x, @y)) , computeLine^#(@line, @m, @acc) -> c_3(computeLine#1^#(@line, @acc, @m)) , computeLine#1^#(::(@x, @xs), @acc, @m) -> c_4(computeLine#2^#(@m, @acc, @x, @xs)) , computeLine#1^#(nil(), @acc, @m) -> c_5() , computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_6(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , computeLine#2^#(nil(), @acc, @x, @xs) -> c_7() , lineMult^#(@n, @l1, @l2) -> c_8(lineMult#1^#(@l1, @l2, @n)) , lineMult#1^#(::(@x, @xs), @l2, @n) -> c_9(lineMult#2^#(@l2, @n, @x, @xs)) , lineMult#1^#(nil(), @l2, @n) -> c_10() , lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_11(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys)) , lineMult#2^#(nil(), @n, @x, @xs) -> c_12(*^#(@x, @n), lineMult^#(@n, @xs, nil())) , matrixMult^#(@m1, @m2) -> c_13(matrixMult#1^#(@m1, @m2)) , matrixMult#1^#(::(@l, @ls), @m2) -> c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) , matrixMult#1^#(nil(), @m2) -> c_15() } Weak DPs: { #mult^#(#0(), #0()) -> c_16() , #mult^#(#0(), #neg(@y)) -> c_17() , #mult^#(#0(), #pos(@y)) -> c_18() , #mult^#(#neg(@x), #0()) -> c_19() , #mult^#(#neg(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_21(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_22() , #mult^#(#pos(@x), #neg(@y)) -> c_23(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_25() , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_27(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_28(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_29(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #natmult^#(#0(), @y) -> c_38() , #natmult^#(#s(@x), @y) -> c_39(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #pred^#(#0()) -> c_30() , #pred^#(#neg(#s(@x))) -> c_31() , #pred^#(#pos(#s(#0()))) -> c_32() , #pred^#(#pos(#s(#s(@x)))) -> c_33() , #succ^#(#0()) -> c_34() , #succ^#(#neg(#s(#0()))) -> c_35() , #succ^#(#neg(#s(#s(@x)))) -> c_36() , #succ^#(#pos(#s(@x))) -> c_37() , #natadd^#(#0(), @y) -> c_40() , #natadd^#(#s(@x), @y) -> c_41(#natadd^#(@x, @y)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) , matrixMult#1(nil(), @m2) -> nil() , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,5,7,10,15} by applications of Pre({1,2,5,7,10,15}) = {3,4,8,11,12,13}. Here rules are labeled as follows: DPs: { 1: *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , 2: +^#(@x, @y) -> c_2(#add^#(@x, @y)) , 3: computeLine^#(@line, @m, @acc) -> c_3(computeLine#1^#(@line, @acc, @m)) , 4: computeLine#1^#(::(@x, @xs), @acc, @m) -> c_4(computeLine#2^#(@m, @acc, @x, @xs)) , 5: computeLine#1^#(nil(), @acc, @m) -> c_5() , 6: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_6(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , 7: computeLine#2^#(nil(), @acc, @x, @xs) -> c_7() , 8: lineMult^#(@n, @l1, @l2) -> c_8(lineMult#1^#(@l1, @l2, @n)) , 9: lineMult#1^#(::(@x, @xs), @l2, @n) -> c_9(lineMult#2^#(@l2, @n, @x, @xs)) , 10: lineMult#1^#(nil(), @l2, @n) -> c_10() , 11: lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_11(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys)) , 12: lineMult#2^#(nil(), @n, @x, @xs) -> c_12(*^#(@x, @n), lineMult^#(@n, @xs, nil())) , 13: matrixMult^#(@m1, @m2) -> c_13(matrixMult#1^#(@m1, @m2)) , 14: matrixMult#1^#(::(@l, @ls), @m2) -> c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) , 15: matrixMult#1^#(nil(), @m2) -> c_15() , 16: #mult^#(#0(), #0()) -> c_16() , 17: #mult^#(#0(), #neg(@y)) -> c_17() , 18: #mult^#(#0(), #pos(@y)) -> c_18() , 19: #mult^#(#neg(@x), #0()) -> c_19() , 20: #mult^#(#neg(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y)) , 21: #mult^#(#neg(@x), #pos(@y)) -> c_21(#natmult^#(@x, @y)) , 22: #mult^#(#pos(@x), #0()) -> c_22() , 23: #mult^#(#pos(@x), #neg(@y)) -> c_23(#natmult^#(@x, @y)) , 24: #mult^#(#pos(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y)) , 25: #add^#(#0(), @y) -> c_25() , 26: #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) , 27: #add^#(#neg(#s(#s(@x))), @y) -> c_27(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 28: #add^#(#pos(#s(#0())), @y) -> c_28(#succ^#(@y)) , 29: #add^#(#pos(#s(#s(@x))), @y) -> c_29(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 30: #natmult^#(#0(), @y) -> c_38() , 31: #natmult^#(#s(@x), @y) -> c_39(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , 32: #pred^#(#0()) -> c_30() , 33: #pred^#(#neg(#s(@x))) -> c_31() , 34: #pred^#(#pos(#s(#0()))) -> c_32() , 35: #pred^#(#pos(#s(#s(@x)))) -> c_33() , 36: #succ^#(#0()) -> c_34() , 37: #succ^#(#neg(#s(#0()))) -> c_35() , 38: #succ^#(#neg(#s(#s(@x)))) -> c_36() , 39: #succ^#(#pos(#s(@x))) -> c_37() , 40: #natadd^#(#0(), @y) -> c_40() , 41: #natadd^#(#s(@x), @y) -> c_41(#natadd^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { computeLine^#(@line, @m, @acc) -> c_3(computeLine#1^#(@line, @acc, @m)) , computeLine#1^#(::(@x, @xs), @acc, @m) -> c_4(computeLine#2^#(@m, @acc, @x, @xs)) , computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_6(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , lineMult^#(@n, @l1, @l2) -> c_8(lineMult#1^#(@l1, @l2, @n)) , lineMult#1^#(::(@x, @xs), @l2, @n) -> c_9(lineMult#2^#(@l2, @n, @x, @xs)) , lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_11(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys)) , lineMult#2^#(nil(), @n, @x, @xs) -> c_12(*^#(@x, @n), lineMult^#(@n, @xs, nil())) , matrixMult^#(@m1, @m2) -> c_13(matrixMult#1^#(@m1, @m2)) , matrixMult#1^#(::(@l, @ls), @m2) -> c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) } Weak DPs: { *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_16() , #mult^#(#0(), #neg(@y)) -> c_17() , #mult^#(#0(), #pos(@y)) -> c_18() , #mult^#(#neg(@x), #0()) -> c_19() , #mult^#(#neg(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_21(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_22() , #mult^#(#pos(@x), #neg(@y)) -> c_23(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y)) , +^#(@x, @y) -> c_2(#add^#(@x, @y)) , #add^#(#0(), @y) -> c_25() , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_27(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_28(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_29(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , computeLine#1^#(nil(), @acc, @m) -> c_5() , computeLine#2^#(nil(), @acc, @x, @xs) -> c_7() , lineMult#1^#(nil(), @l2, @n) -> c_10() , matrixMult#1^#(nil(), @m2) -> c_15() , #natmult^#(#0(), @y) -> c_38() , #natmult^#(#s(@x), @y) -> c_39(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #pred^#(#0()) -> c_30() , #pred^#(#neg(#s(@x))) -> c_31() , #pred^#(#pos(#s(#0()))) -> c_32() , #pred^#(#pos(#s(#s(@x)))) -> c_33() , #succ^#(#0()) -> c_34() , #succ^#(#neg(#s(#0()))) -> c_35() , #succ^#(#neg(#s(#s(@x)))) -> c_36() , #succ^#(#pos(#s(@x))) -> c_37() , #natadd^#(#0(), @y) -> c_40() , #natadd^#(#s(@x), @y) -> c_41(#natadd^#(@x, @y)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) , matrixMult#1(nil(), @m2) -> nil() , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { *^#(@x, @y) -> c_1(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_16() , #mult^#(#0(), #neg(@y)) -> c_17() , #mult^#(#0(), #pos(@y)) -> c_18() , #mult^#(#neg(@x), #0()) -> c_19() , #mult^#(#neg(@x), #neg(@y)) -> c_20(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_21(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_22() , #mult^#(#pos(@x), #neg(@y)) -> c_23(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_24(#natmult^#(@x, @y)) , +^#(@x, @y) -> c_2(#add^#(@x, @y)) , #add^#(#0(), @y) -> c_25() , #add^#(#neg(#s(#0())), @y) -> c_26(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_27(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_28(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_29(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , computeLine#1^#(nil(), @acc, @m) -> c_5() , computeLine#2^#(nil(), @acc, @x, @xs) -> c_7() , lineMult#1^#(nil(), @l2, @n) -> c_10() , matrixMult#1^#(nil(), @m2) -> c_15() , #natmult^#(#0(), @y) -> c_38() , #natmult^#(#s(@x), @y) -> c_39(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #pred^#(#0()) -> c_30() , #pred^#(#neg(#s(@x))) -> c_31() , #pred^#(#pos(#s(#0()))) -> c_32() , #pred^#(#pos(#s(#s(@x)))) -> c_33() , #succ^#(#0()) -> c_34() , #succ^#(#neg(#s(#0()))) -> c_35() , #succ^#(#neg(#s(#s(@x)))) -> c_36() , #succ^#(#pos(#s(@x))) -> c_37() , #natadd^#(#0(), @y) -> c_40() , #natadd^#(#s(@x), @y) -> c_41(#natadd^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { computeLine^#(@line, @m, @acc) -> c_3(computeLine#1^#(@line, @acc, @m)) , computeLine#1^#(::(@x, @xs), @acc, @m) -> c_4(computeLine#2^#(@m, @acc, @x, @xs)) , computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_6(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , lineMult^#(@n, @l1, @l2) -> c_8(lineMult#1^#(@l1, @l2, @n)) , lineMult#1^#(::(@x, @xs), @l2, @n) -> c_9(lineMult#2^#(@l2, @n, @x, @xs)) , lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_11(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys)) , lineMult#2^#(nil(), @n, @x, @xs) -> c_12(*^#(@x, @n), lineMult^#(@n, @xs, nil())) , matrixMult^#(@m1, @m2) -> c_13(matrixMult#1^#(@m1, @m2)) , matrixMult#1^#(::(@l, @ls), @m2) -> c_14(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) , matrixMult#1(nil(), @m2) -> nil() , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_11(+^#(*(@x, @n), @y), *^#(@x, @n), lineMult^#(@n, @xs, @ys)) , lineMult#2^#(nil(), @n, @x, @xs) -> c_12(*^#(@x, @n), lineMult^#(@n, @xs, nil())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { computeLine^#(@line, @m, @acc) -> c_1(computeLine#1^#(@line, @acc, @m)) , computeLine#1^#(::(@x, @xs), @acc, @m) -> c_2(computeLine#2^#(@m, @acc, @x, @xs)) , computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , lineMult^#(@n, @l1, @l2) -> c_4(lineMult#1^#(@l1, @l2, @n)) , lineMult#1^#(::(@x, @xs), @l2, @n) -> c_5(lineMult#2^#(@l2, @n, @x, @xs)) , lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_6(lineMult^#(@n, @xs, @ys)) , lineMult#2^#(nil(), @n, @x, @xs) -> c_7(lineMult^#(@n, @xs, nil())) , matrixMult^#(@m1, @m2) -> c_8(matrixMult#1^#(@m1, @m2)) , matrixMult#1^#(::(@l, @ls), @m2) -> c_9(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) , matrixMult#1(nil(), @m2) -> nil() , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { computeLine^#(@line, @m, @acc) -> c_1(computeLine#1^#(@line, @acc, @m)) , computeLine#1^#(::(@x, @xs), @acc, @m) -> c_2(computeLine#2^#(@m, @acc, @x, @xs)) , computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , lineMult^#(@n, @l1, @l2) -> c_4(lineMult#1^#(@l1, @l2, @n)) , lineMult#1^#(::(@x, @xs), @l2, @n) -> c_5(lineMult#2^#(@l2, @n, @x, @xs)) , lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_6(lineMult^#(@n, @xs, @ys)) , lineMult#2^#(nil(), @n, @x, @xs) -> c_7(lineMult^#(@n, @xs, nil())) , matrixMult^#(@m1, @m2) -> c_8(matrixMult#1^#(@m1, @m2)) , matrixMult#1^#(::(@l, @ls), @m2) -> c_9(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'trivial' failed due to the following reason: We use the processor 'matrix interpretation of dimension 3' to orient following rules strictly. DPs: { 9: matrixMult#1^#(::(@l, @ls), @m2) -> c_9(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) } Trs: { lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1, 2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [0] [*](x1, x2) = [0] [0] [0] [#mult](x1, x2) = [0] [0] [1 0 0] [0] [+](x1, x2) = [0 1 0] x2 + [0] [0 0 1] [0] [1 0 0] [0] [#add](x1, x2) = [0 1 0] x2 + [0] [0 0 1] [0] [1 1 1] [1 1 0] [1] [::](x1, x2) = [0 0 0] x1 + [0 1 1] x2 + [0] [0 0 0] [0 0 0] [0] [1] [nil] = [0] [0] [1 1 1] [1 0 0] [0] [lineMult](x1, x2, x3) = [0 0 0] x2 + [0 0 0] x3 + [0] [0 0 0] [0 0 0] [0] [1 1 0] [1 0 0] [0] [lineMult#1](x1, x2, x3) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [1 0 0] [1 1 1] [1] [lineMult#2](x1, x2, x3, x4) = [0 0 0] x1 + [0 0 0] x4 + [0] [0 0 0] [0 0 0] [0] [0] [#0] = [0] [0] [0] [#s](x1) = [0] [0] [1 0 1] [0] [#neg](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [#pred](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [#pos](x1) = [0 1 1] x1 + [0] [0 0 0] [0] [0] [#succ](x1) = [0] [0] [0] [#natmult](x1, x2) = [0] [0] [1 1 1] [0] [#natadd](x1, x2) = [0 1 1] x2 + [0] [0 1 1] [0] [0] [*^#](x1, x2) = [0] [0] [0] [#mult^#](x1, x2) = [0] [0] [0] [+^#](x1, x2) = [0] [0] [0] [#add^#](x1, x2) = [0] [0] [1 0 0] [0 1 0] [0] [computeLine^#](x1, x2, x3) = [0 0 0] x1 + [0 0 0] x3 + [0] [0 0 0] [0 0 0] [0] [1 0 0] [0 1 0] [0] [computeLine#1^#](x1, x2, x3) = [1 1 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [0 0 0] [0 1 0] [1 0 0] [1] [computeLine#2^#](x1, x2, x3, x4) = [1 0 0] x1 + [0 1 0] x2 + [1 0 0] x4 + [1] [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] [1] [lineMult^#](x1, x2, x3) = [0 0 0] x3 + [1] [0 0 0] [0] [0 0 0] [0 1 0] [1] [lineMult#1^#](x1, x2, x3) = [0 0 0] x1 + [0 0 0] x2 + [0] [1 0 0] [0 0 0] [0] [0 1 0] [1] [lineMult#2^#](x1, x2, x3, x4) = [1 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [1 1 0] [0] [matrixMult^#](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [1] [0 0 0] [0 0 0] [1] [1 0 0] [1 1 0] [0] [matrixMult#1^#](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [1] [0] [#natmult^#](x1, x2) = [0] [0] [0] [#pred^#](x1) = [0] [0] [0] [#succ^#](x1) = [0] [0] [0] [#natadd^#](x1, x2) = [0] [0] [1 0 0] [0] [c_1](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_2](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 1] [1 0 0] [0] [c_3](x1, x2) = [1 1 0] x1 + [0 1 0] x2 + [1] [0 0 0] [0 0 0] [0] [1 0 0] [0] [c_4](x1) = [0 0 0] x1 + [1] [0 0 0] [0] [1 0 0] [0] [c_5](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_6](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 1] [0] [c_7](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_8](x1) = [0 0 0] x1 + [0] [0 0 0] [1] [1 1 0] [1 0 0] [0] [c_9](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] This order satisfies following ordering constraints [*(@x, @y)] = [0] [0] [0] >= [0] [0] [0] = [#mult(@x, @y)] [#mult(#0(), #0())] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#0(), #neg(@y))] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#0(), #pos(@y))] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#neg(@x), #0())] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [0] [0] [0] >= [0] [0] [0] = [#pos(#natmult(@x, @y))] [#mult(#neg(@x), #pos(@y))] = [0] [0] [0] >= [0] [0] [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [0] [0] [0] >= [0] [0] [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #pos(@y))] = [0] [0] [0] >= [0] [0] [0] = [#pos(#natmult(@x, @y))] [+(@x, @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] = [#add(@x, @y)] [#add(#0(), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [1 0 0] [0] [0 0 0] @y + [0] [0 0 0] [0] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [1 0 0] [0] [0 0 0] @y + [0] [0 0 0] [0] = [#pred(#add(#pos(#s(@x)), @y))] [#add(#pos(#s(#0())), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [0] [0] [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [0] [0] [0] = [#succ(#add(#pos(#s(@x)), @y))] [lineMult(@n, @l1, @l2)] = [1 1 1] [1 0 0] [0] [0 0 0] @l1 + [0 0 0] @l2 + [0] [0 0 0] [0 0 0] [0] >= [1 1 0] [1 0 0] [0] [0 0 0] @l1 + [0 0 0] @l2 + [0] [0 0 0] [0 0 0] [0] = [lineMult#1(@l1, @l2, @n)] [lineMult#1(::(@x, @xs), @l2, @n)] = [1 0 0] [1 1 1] [1 2 1] [1] [0 0 0] @l2 + [0 0 0] @x + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0 0 0] [0] >= [1 0 0] [1 1 1] [1] [0 0 0] @l2 + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1 0 0] [1] [0 0 0] @l2 + [0] [0 0 0] [0] >= [1] [0] [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1 1 1] [1 1 1] [1 1 0] [2] [0 0 0] @xs + [0 0 0] @y + [0 0 0] @ys + [0] [0 0 0] [0 0 0] [0 0 0] [0] > [1 1 1] [1 1 1] [1 0 0] [1] [0 0 0] @xs + [0 0 0] @y + [0 0 0] @ys + [0] [0 0 0] [0 0 0] [0 0 0] [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [1 1 1] [2] [0 0 0] @xs + [0] [0 0 0] [0] >= [1 1 1] [2] [0 0 0] @xs + [0] [0 0 0] [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [#pred(#0())] = [0] [0] [0] >= [0] [0] [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [0] [0] [0] >= [0] [0] [0] = [#neg(#s(#s(@x)))] [#pred(#pos(#s(#0())))] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [0] [0] [0] >= [0] [0] [0] = [#pos(#s(@x))] [#succ(#0())] = [0] [0] [0] >= [0] [0] [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [0] [0] [0] >= [0] [0] [0] = [#neg(#s(@x))] [#succ(#pos(#s(@x)))] = [0] [0] [0] >= [0] [0] [0] = [#pos(#s(#s(@x)))] [#natmult(#0(), @y)] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#natmult(#s(@x), @y)] = [0] [0] [0] >= [0] [0] [0] = [#natadd(@y, #natmult(@x, @y))] [#natadd(#0(), @y)] = [1 1 1] [0] [0 1 1] @y + [0] [0 1 1] [0] >= [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] = [@y] [#natadd(#s(@x), @y)] = [1 1 1] [0] [0 1 1] @y + [0] [0 1 1] [0] >= [0] [0] [0] = [#s(#natadd(@x, @y))] [computeLine^#(@line, @m, @acc)] = [0 1 0] [1 0 0] [0] [0 0 0] @acc + [0 0 0] @line + [0] [0 0 0] [0 0 0] [0] >= [0 1 0] [1 0 0] [0] [0 0 0] @acc + [0 0 0] @line + [0] [0 0 0] [0 0 0] [0] = [c_1(computeLine#1^#(@line, @acc, @m))] [computeLine#1^#(::(@x, @xs), @acc, @m)] = [0 1 0] [1 1 1] [1 1 0] [1] [0 0 0] @acc + [1 1 1] @x + [1 2 1] @xs + [1] [0 0 0] [0 0 0] [0 0 0] [0] >= [0 1 0] [1 0 0] [1] [0 0 0] @acc + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0] = [c_2(computeLine#2^#(@m, @acc, @x, @xs))] [computeLine#2^#(::(@l, @ls), @acc, @x, @xs)] = [0 1 0] [0 0 0] [0 0 0] [1 0 0] [1] [0 1 0] @acc + [1 1 1] @l + [1 1 0] @ls + [1 0 0] @xs + [2] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0] >= [0 1 0] [1 0 0] [1] [0 0 0] @acc + [1 0 0] @xs + [2] [0 0 0] [0 0 0] [0] = [c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc))] [lineMult^#(@n, @l1, @l2)] = [0 1 0] [1] [0 0 0] @l2 + [1] [0 0 0] [0] >= [0 1 0] [1] [0 0 0] @l2 + [1] [0 0 0] [0] = [c_4(lineMult#1^#(@l1, @l2, @n))] [lineMult#1^#(::(@x, @xs), @l2, @n)] = [0 1 0] [0 0 0] [0 0 0] [1] [0 0 0] @l2 + [0 0 0] @x + [0 0 0] @xs + [0] [0 0 0] [1 1 1] [1 1 0] [1] >= [0 1 0] [1] [0 0 0] @l2 + [0] [0 0 0] [0] = [c_5(lineMult#2^#(@l2, @n, @x, @xs))] [lineMult#2^#(::(@y, @ys), @n, @x, @xs)] = [0 0 0] [0 1 1] [1] [1 1 1] @y + [1 1 0] @ys + [1] [0 0 0] [0 0 0] [0] >= [0 1 0] [1] [0 0 0] @ys + [0] [0 0 0] [0] = [c_6(lineMult^#(@n, @xs, @ys))] [lineMult#2^#(nil(), @n, @x, @xs)] = [1] [1] [0] >= [1] [0] [0] = [c_7(lineMult^#(@n, @xs, nil()))] [matrixMult^#(@m1, @m2)] = [1 0 0] [1 1 0] [0] [0 0 0] @m1 + [0 0 0] @m2 + [1] [0 0 0] [0 0 0] [1] >= [1 0 0] [1 1 0] [0] [0 0 0] @m1 + [0 0 0] @m2 + [0] [0 0 0] [0 0 0] [1] = [c_8(matrixMult#1^#(@m1, @m2))] [matrixMult#1^#(::(@l, @ls), @m2)] = [1 1 1] [1 1 0] [1 1 0] [1] [0 0 0] @l + [0 0 0] @ls + [0 0 0] @m2 + [0] [0 0 0] [0 0 0] [0 0 0] [1] > [1 0 0] [1 0 0] [1 1 0] [0] [0 0 0] @l + [0 0 0] @ls + [0 0 0] @m2 + [0] [0 0 0] [0 0 0] [0 0 0] [0] = [c_9(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))] Consider the set of all dependency pairs DPs: { 1: computeLine^#(@line, @m, @acc) -> c_1(computeLine#1^#(@line, @acc, @m)) , 2: computeLine#1^#(::(@x, @xs), @acc, @m) -> c_2(computeLine#2^#(@m, @acc, @x, @xs)) , 3: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , 4: lineMult^#(@n, @l1, @l2) -> c_4(lineMult#1^#(@l1, @l2, @n)) , 5: lineMult#1^#(::(@x, @xs), @l2, @n) -> c_5(lineMult#2^#(@l2, @n, @x, @xs)) , 6: lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_6(lineMult^#(@n, @xs, @ys)) , 7: lineMult#2^#(nil(), @n, @x, @xs) -> c_7(lineMult^#(@n, @xs, nil())) , 8: matrixMult^#(@m1, @m2) -> c_8(matrixMult#1^#(@m1, @m2)) , 9: matrixMult#1^#(::(@l, @ls), @m2) -> c_9(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) } Processor 'matrix interpretation of dimension 3' induces the complexity certificate YES(?,O(n^3)) on application of dependency pairs {9}. These cover all (indirect) predecessors of dependency pairs {8,9}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { computeLine^#(@line, @m, @acc) -> c_1(computeLine#1^#(@line, @acc, @m)) , computeLine#1^#(::(@x, @xs), @acc, @m) -> c_2(computeLine#2^#(@m, @acc, @x, @xs)) , computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , lineMult^#(@n, @l1, @l2) -> c_4(lineMult#1^#(@l1, @l2, @n)) , lineMult#1^#(::(@x, @xs), @l2, @n) -> c_5(lineMult#2^#(@l2, @n, @x, @xs)) , lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_6(lineMult^#(@n, @xs, @ys)) , lineMult#2^#(nil(), @n, @x, @xs) -> c_7(lineMult^#(@n, @xs, nil())) } Weak DPs: { matrixMult^#(@m1, @m2) -> c_8(matrixMult#1^#(@m1, @m2)) , matrixMult#1^#(::(@l, @ls), @m2) -> c_9(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 3' to orient following rules strictly. DPs: { 1: computeLine^#(@line, @m, @acc) -> c_1(computeLine#1^#(@line, @acc, @m)) } Trs: { lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1, 2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [0] [*](x1, x2) = [0] [0] [0] [#mult](x1, x2) = [0] [0] [1 0 0] [0] [+](x1, x2) = [0 1 0] x2 + [0] [0 0 1] [0] [1 0 0] [0] [#add](x1, x2) = [0 1 0] x2 + [0] [0 0 1] [0] [1 0 0] [1 0 0] [1] [::](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 1] [0] [1] [nil] = [0] [0] [1 0 1] [1 0 0] [0] [lineMult](x1, x2, x3) = [0 0 0] x2 + [0 0 0] x3 + [0] [0 0 0] [0 0 0] [0] [1 0 1] [1 0 0] [0] [lineMult#1](x1, x2, x3) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [1 0 0] [1 0 0] [1 0 1] [1] [lineMult#2](x1, x2, x3, x4) = [0 0 0] x1 + [0 0 0] x3 + [0 0 0] x4 + [0] [0 0 0] [0 0 0] [0 0 0] [0] [0] [#0] = [0] [0] [0 0 0] [0] [#s](x1) = [0 0 0] x1 + [0] [0 1 0] [0] [0] [#neg](x1) = [0] [0] [0] [#pred](x1) = [0] [0] [0] [#pos](x1) = [0] [0] [0] [#succ](x1) = [0] [0] [0 0 1] [0] [#natmult](x1, x2) = [1 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [#natadd](x1, x2) = [0 0 0] x2 + [0] [0 0 0] [0] [0] [*^#](x1, x2) = [0] [0] [0] [#mult^#](x1, x2) = [0] [0] [0] [+^#](x1, x2) = [0] [0] [0] [#add^#](x1, x2) = [0] [0] [1 0 0] [0 0 0] [0 1 1] [1] [computeLine^#](x1, x2, x3) = [0 0 0] x1 + [0 0 1] x2 + [1 0 0] x3 + [0] [0 0 0] [0 0 1] [0 0 0] [1] [1 0 0] [0 0 1] [0 0 0] [0] [computeLine#1^#](x1, x2, x3) = [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [1] [1 0 0] [0 0 0] [1 0 0] [1] [0 0 0] [0 0 1] [1 0 0] [1] [computeLine#2^#](x1, x2, x3, x4) = [1 0 0] x1 + [0 0 0] x2 + [1 0 0] x4 + [1] [1 0 1] [0 0 0] [0 0 0] [1] [0 0 1] [0] [lineMult^#](x1, x2, x3) = [0 0 0] x3 + [1] [0 1 1] [0] [0 0 0] [0 0 1] [0] [lineMult#1^#](x1, x2, x3) = [1 0 0] x1 + [0 0 0] x2 + [1] [0 0 0] [0 0 0] [1] [0 0 1] [0] [lineMult#2^#](x1, x2, x3, x4) = [0 0 0] x1 + [1] [0 0 0] [1] [1 0 1] [1 1 1] [0] [matrixMult^#](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [1 0 1] [1 1 1] [0] [matrixMult#1^#](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [0] [#natmult^#](x1, x2) = [0] [0] [0] [#pred^#](x1) = [0] [0] [0] [#succ^#](x1) = [0] [0] [0] [#natadd^#](x1, x2) = [0] [0] [1 0 0] [0] [c_1](x1) = [0 0 0] x1 + [0] [0 0 0] [1] [1 0 0] [0] [c_2](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [1 0 0] [0] [c_3](x1, x2) = [1 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [1 0 0] [0] [c_4](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_5](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_6](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 1] [0] [c_7](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_8](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [1 0 0] [0] [c_9](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] This order satisfies following ordering constraints [*(@x, @y)] = [0] [0] [0] >= [0] [0] [0] = [#mult(@x, @y)] [#mult(#0(), #0())] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#0(), #neg(@y))] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#0(), #pos(@y))] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#neg(@x), #0())] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [0] [0] [0] >= [0] [0] [0] = [#pos(#natmult(@x, @y))] [#mult(#neg(@x), #pos(@y))] = [0] [0] [0] >= [0] [0] [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [0] [0] [0] >= [0] [0] [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #pos(@y))] = [0] [0] [0] >= [0] [0] [0] = [#pos(#natmult(@x, @y))] [+(@x, @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] = [#add(@x, @y)] [#add(#0(), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [0] [0] [0] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [0] [0] [0] = [#pred(#add(#pos(#s(@x)), @y))] [#add(#pos(#s(#0())), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [0] [0] [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [1 0 0] [0] [0 1 0] @y + [0] [0 0 1] [0] >= [0] [0] [0] = [#succ(#add(#pos(#s(@x)), @y))] [lineMult(@n, @l1, @l2)] = [1 0 1] [1 0 0] [0] [0 0 0] @l1 + [0 0 0] @l2 + [0] [0 0 0] [0 0 0] [0] >= [1 0 1] [1 0 0] [0] [0 0 0] @l1 + [0 0 0] @l2 + [0] [0 0 0] [0 0 0] [0] = [lineMult#1(@l1, @l2, @n)] [lineMult#1(::(@x, @xs), @l2, @n)] = [1 0 0] [1 0 0] [1 0 1] [1] [0 0 0] @l2 + [0 0 0] @x + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0 0 0] [0] >= [1 0 0] [1 0 0] [1 0 1] [1] [0 0 0] @l2 + [0 0 0] @x + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0 0 0] [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1 0 0] [1] [0 0 0] @l2 + [0] [0 0 0] [0] >= [1] [0] [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1 0 0] [1 0 1] [1 0 0] [1 0 0] [2] [0 0 0] @x + [0 0 0] @xs + [0 0 0] @y + [0 0 0] @ys + [0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0] > [1 0 1] [1 0 0] [1 0 0] [1] [0 0 0] @xs + [0 0 0] @y + [0 0 0] @ys + [0] [0 0 0] [0 0 0] [0 0 0] [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [1 0 0] [1 0 1] [2] [0 0 0] @x + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0] >= [1 0 1] [2] [0 0 0] @xs + [0] [0 0 0] [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [#pred(#0())] = [0] [0] [0] >= [0] [0] [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [0] [0] [0] >= [0] [0] [0] = [#neg(#s(#s(@x)))] [#pred(#pos(#s(#0())))] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [0] [0] [0] >= [0] [0] [0] = [#pos(#s(@x))] [#succ(#0())] = [0] [0] [0] >= [0] [0] [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] [0] [0] >= [0] [0] [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [0] [0] [0] >= [0] [0] [0] = [#neg(#s(@x))] [#succ(#pos(#s(@x)))] = [0] [0] [0] >= [0] [0] [0] = [#pos(#s(#s(@x)))] [computeLine^#(@line, @m, @acc)] = [0 1 1] [1 0 0] [0 0 0] [1] [1 0 0] @acc + [0 0 0] @line + [0 0 1] @m + [0] [0 0 0] [0 0 0] [0 0 1] [1] > [0 0 1] [1 0 0] [0] [0 0 0] @acc + [0 0 0] @line + [0] [0 0 0] [0 0 0] [1] = [c_1(computeLine#1^#(@line, @acc, @m))] [computeLine#1^#(::(@x, @xs), @acc, @m)] = [0 0 1] [0 0 0] [1 0 0] [1 0 0] [1] [0 0 0] @acc + [0 0 0] @m + [0 0 0] @x + [0 0 0] @xs + [1] [0 0 0] [1 0 0] [1 0 0] [1 0 0] [2] >= [0 0 1] [1 0 0] [1] [0 0 0] @acc + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0] = [c_2(computeLine#2^#(@m, @acc, @x, @xs))] [computeLine#2^#(::(@l, @ls), @acc, @x, @xs)] = [0 0 1] [0 0 0] [0 0 0] [1 0 0] [1] [0 0 0] @acc + [1 0 0] @l + [1 0 0] @ls + [1 0 0] @xs + [2] [0 0 0] [1 0 0] [1 0 1] [0 0 0] [2] >= [0 0 1] [1 0 0] [1] [0 0 0] @acc + [1 0 0] @xs + [1] [0 0 0] [0 0 0] [0] = [c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc))] [lineMult^#(@n, @l1, @l2)] = [0 0 1] [0] [0 0 0] @l2 + [1] [0 1 1] [0] >= [0 0 1] [0] [0 0 0] @l2 + [0] [0 0 0] [0] = [c_4(lineMult#1^#(@l1, @l2, @n))] [lineMult#1^#(::(@x, @xs), @l2, @n)] = [0 0 1] [0 0 0] [0 0 0] [0] [0 0 0] @l2 + [1 0 0] @x + [1 0 0] @xs + [2] [0 0 0] [0 0 0] [0 0 0] [1] >= [0 0 1] [0] [0 0 0] @l2 + [0] [0 0 0] [0] = [c_5(lineMult#2^#(@l2, @n, @x, @xs))] [lineMult#2^#(::(@y, @ys), @n, @x, @xs)] = [0 0 1] [0] [0 0 0] @ys + [1] [0 0 0] [1] >= [0 0 1] [0] [0 0 0] @ys + [0] [0 0 0] [0] = [c_6(lineMult^#(@n, @xs, @ys))] [lineMult#2^#(nil(), @n, @x, @xs)] = [0] [1] [1] >= [0] [0] [0] = [c_7(lineMult^#(@n, @xs, nil()))] [matrixMult^#(@m1, @m2)] = [1 0 1] [1 1 1] [0] [0 0 0] @m1 + [0 0 0] @m2 + [0] [0 0 0] [0 0 0] [0] >= [1 0 1] [1 1 1] [0] [0 0 0] @m1 + [0 0 0] @m2 + [0] [0 0 0] [0 0 0] [0] = [c_8(matrixMult#1^#(@m1, @m2))] [matrixMult#1^#(::(@l, @ls), @m2)] = [1 0 0] [1 0 1] [1 1 1] [1] [0 0 0] @l + [0 0 0] @ls + [0 0 0] @m2 + [0] [0 0 0] [0 0 0] [0 0 0] [0] >= [1 0 0] [1 0 1] [1 1 1] [1] [0 0 0] @l + [0 0 0] @ls + [0 0 0] @m2 + [0] [0 0 0] [0 0 0] [0 0 0] [0] = [c_9(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2))] Consider the set of all dependency pairs DPs: { 1: computeLine^#(@line, @m, @acc) -> c_1(computeLine#1^#(@line, @acc, @m)) , 2: computeLine#1^#(::(@x, @xs), @acc, @m) -> c_2(computeLine#2^#(@m, @acc, @x, @xs)) , 3: computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , 4: lineMult^#(@n, @l1, @l2) -> c_4(lineMult#1^#(@l1, @l2, @n)) , 5: lineMult#1^#(::(@x, @xs), @l2, @n) -> c_5(lineMult#2^#(@l2, @n, @x, @xs)) , 6: lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_6(lineMult^#(@n, @xs, @ys)) , 7: lineMult#2^#(nil(), @n, @x, @xs) -> c_7(lineMult^#(@n, @xs, nil())) , 8: matrixMult^#(@m1, @m2) -> c_8(matrixMult#1^#(@m1, @m2)) , 9: matrixMult#1^#(::(@l, @ls), @m2) -> c_9(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) } Processor 'matrix interpretation of dimension 3' induces the complexity certificate YES(?,O(n^3)) on application of dependency pairs {1}. These cover all (indirect) predecessors of dependency pairs {1,2,3}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { lineMult^#(@n, @l1, @l2) -> c_4(lineMult#1^#(@l1, @l2, @n)) , lineMult#1^#(::(@x, @xs), @l2, @n) -> c_5(lineMult#2^#(@l2, @n, @x, @xs)) , lineMult#2^#(::(@y, @ys), @n, @x, @xs) -> c_6(lineMult^#(@n, @xs, @ys)) , lineMult#2^#(nil(), @n, @x, @xs) -> c_7(lineMult^#(@n, @xs, nil())) } Weak DPs: { computeLine^#(@line, @m, @acc) -> c_1(computeLine#1^#(@line, @acc, @m)) , computeLine#1^#(::(@x, @xs), @acc, @m) -> c_2(computeLine#2^#(@m, @acc, @x, @xs)) , computeLine#2^#(::(@l, @ls), @acc, @x, @xs) -> c_3(computeLine^#(@xs, @ls, lineMult(@x, @l, @acc)), lineMult^#(@x, @l, @acc)) , matrixMult^#(@m1, @m2) -> c_8(matrixMult#1^#(@m1, @m2)) , matrixMult#1^#(::(@l, @ls), @m2) -> c_9(computeLine^#(@l, @m2, nil()), matrixMult^#(@ls, @m2)) } Weak Trs: { *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Sequentially' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..